Problem:
 foo(0(x1)) -> 0(s(p(p(p(s(s(s(p(s(x1))))))))))
 foo(s(x1)) -> p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))))))
 bar(0(x1)) -> 0(p(s(s(s(x1)))))
 bar(s(x1)) -> p(s(p(p(s(s(foo(s(p(p(s(s(x1))))))))))))
 p(p(s(x1))) -> p(x1)
 p(s(x1)) -> x1
 p(0(x1)) -> 0(s(s(s(s(x1)))))

Proof:
 Bounds Processor:
  bound: 4
  enrichment: match
  automaton:
   final states: {5,4,3}
   transitions:
    02(223) -> 224*
    01(15) -> 16*
    01(114) -> 115*
    01(86) -> 87*
    03(247) -> 248*
    s1(45) -> 46*
    s1(35) -> 36*
    s1(30) -> 31*
    s1(10) -> 11*
    s1(92) -> 93*
    s1(52) -> 53*
    s1(47) -> 48*
    s1(42) -> 43*
    s1(37) -> 38*
    s1(84) -> 85*
    s1(44) -> 45*
    s1(14) -> 15*
    s1(9) -> 10*
    s1(96) -> 97*
    s1(6) -> 7*
    s1(113) -> 114*
    s1(93) -> 94*
    s1(83) -> 84*
    s1(48) -> 49*
    s1(38) -> 39*
    s1(8) -> 9*
    s1(90) -> 91*
    s3(242) -> 243*
    s3(266) -> 267*
    s3(246) -> 247*
    s3(241) -> 242*
    s3(238) -> 239*
    s3(240) -> 241*
    p1(50) -> 51*
    p1(40) -> 41*
    p1(97) -> 98*
    p1(32) -> 33*
    p1(12) -> 13*
    p1(7) -> 8*
    p1(94) -> 95*
    p1(89) -> 90*
    p1(49) -> 50*
    p1(39) -> 40*
    p1(51) -> 52*
    p1(46) -> 47*
    p1(36) -> 37*
    p1(11) -> 12*
    p1(88) -> 89*
    p1(53) -> 54*
    p1(43) -> 44*
    p1(33) -> 34*
    p1(13) -> 14*
    p1(95) -> 96*
    p1(85) -> 86*
    p4(276) -> 277*
    p4(270) -> 271*
    foo1(91) -> 92*
    foo1(41) -> 42*
    bar1(34) -> 35*
    p2(182) -> 183*
    p2(172) -> 173*
    p2(137) -> 138*
    p2(127) -> 128*
    p2(117) -> 118*
    p2(219) -> 220*
    p2(174) -> 175*
    p2(139) -> 140*
    p2(134) -> 135*
    p2(124) -> 125*
    p2(221) -> 222*
    p2(141) -> 142*
    p2(131) -> 132*
    p2(121) -> 122*
    p2(188) -> 189*
    p2(138) -> 139*
    p2(128) -> 129*
    p2(220) -> 221*
    p2(215) -> 216*
    p2(200) -> 201*
    p2(190) -> 191*
    p2(180) -> 181*
    p2(120) -> 121*
    foo0(2) -> 3*
    foo0(1) -> 3*
    s2(222) -> 223*
    s2(217) -> 218*
    s2(132) -> 133*
    s2(214) -> 215*
    s2(119) -> 120*
    s2(251) -> 252*
    s2(216) -> 217*
    s2(136) -> 137*
    s2(126) -> 127*
    s2(116) -> 117*
    s2(268) -> 269*
    s2(218) -> 219*
    s2(133) -> 134*
    s2(123) -> 124*
    s2(118) -> 119*
    s2(140) -> 141*
    s2(135) -> 136*
    s2(130) -> 131*
    s2(125) -> 126*
    00(2) -> 1*
    00(1) -> 1*
    foo2(129) -> 130*
    s0(2) -> 2*
    s0(1) -> 2*
    bar2(122) -> 123*
    p0(2) -> 5*
    p0(1) -> 5*
    p3(264) -> 265*
    p3(244) -> 245*
    p3(239) -> 240*
    p3(204) -> 205*
    p3(194) -> 195*
    p3(236) -> 237*
    p3(206) -> 207*
    p3(243) -> 244*
    p3(245) -> 246*
    p3(210) -> 211*
    bar0(2) -> 4*
    bar0(1) -> 4*
    1 -> 5,30
    2 -> 5,6
    6 -> 175,8
    7 -> 83*
    8 -> 183,34
    9 -> 189,33,182
    10 -> 12,188,32
    16 -> 3*
    30 -> 175,8
    31 -> 7*
    35 -> 37*
    37 -> 123,125,205,173
    38 -> 40,172
    41 -> 35*
    42 -> 44*
    44 -> 201*
    45 -> 47*
    47 -> 191,51,200
    48 -> 50,190
    52 -> 54*
    54 -> 3*
    83 -> 89,174
    84 -> 86,88
    85 -> 113*
    86 -> 214*
    87 -> 123,125,205,35,37,41,4
    90 -> 116*
    92 -> 181*
    93 -> 95,180
    96 -> 98,4
    98 -> 37,41,4
    115 -> 5*
    116 -> 118*
    118 -> 207,122
    119 -> 121,206
    123 -> 125*
    125 -> 205,129
    126 -> 128,204
    130 -> 132*
    132 -> 211,140,142
    133 -> 135*
    135 -> 195,210
    136 -> 138,194
    140 -> 142,92
    142 -> 92*
    173 -> 41*
    175 -> 90*
    181 -> 96*
    183 -> 14,34
    189 -> 13*
    191 -> 51*
    195 -> 139*
    201 -> 52*
    205 -> 129*
    207 -> 122*
    211 -> 140,142,96
    214 -> 216*
    216 -> 265,222
    217 -> 237,221,264
    218 -> 220,236
    223 -> 251,238
    224 -> 130,132,140,181,98,37,123,129,42,44,52,3
    237 -> 221*
    238 -> 240*
    240 -> 277,246
    241 -> 271,245,276
    242 -> 244,270
    247 -> 268,266
    248 -> 130,132,140,181,98,37,123,129
    251 -> 216*
    252 -> 215*
    265 -> 222*
    266 -> 240*
    267 -> 239*
    268 -> 216,265
    269 -> 215*
    271 -> 245*
    277 -> 246*
  problem:
   
  Qed